#include "Problem.h"

void Clause::addVariableParity(int i) {
    variables_.push_back(i);
}

Clause::VariableConstIterator Clause::getVariableBegin() const {
    return variables_.begin();
}

Clause::VariableConstIterator Clause::getVariableEnd() const {
    return variables_.end();
}

int Clause::getNumVariables() const {
    return variables_.size();
}

bool Clause::getParity(Variable v) const {
    return (v > 0);
}

Problem::~Problem() {
    for (size_t i = 0; i < allClauses_.size(); i++) {
    //    if(allClauses_[i]) delete allClauses_[i]; TODO: causes glibc problem
        allClauses_[i] = 0;
    }
}

void Problem::addClause(Clause* c) {
    allClauses_.push_back(c);
    std::for_each(c->getVariableBegin(), c->getVariableEnd(), [c, this](const Variable& v) {
        varToClauseMap_.insert(std::make_pair(std::abs(v), c));
    });
}

Problem::VarToClauseMapIteratorPair Problem::getClausesContaining(const Variable& v) const {
    return varToClauseMap_.equal_range(std::abs(v));
}

Problem::ClauseConstIterator Problem::getClauseBegin() const {
    return allClauses_.begin();
}

Problem::ClauseConstIterator Problem::getClauseEnd() const {
    return allClauses_.end();
}

int Problem::getNumVariables() const {
    return varToClauseMap_.rbegin()->first;
}

Solution::Solution(const Problem& p) 
: problem_(p) {
    // initializes with all variables set to false
    parity_.resize(problem_.getNumVariables());
}

const Problem& Solution::getProblem() const {
    return problem_;
}

bool Solution::getParityOfVariable(Variable v) const {
    assert((v > 0) && "Variable without parity is expected here");
    return parity_[v-1];
}

void Solution::flipVariable(Variable v) {
    bool b = parity_[v-1];
    parity_[v-1] = !b;
}

bool Solution::isSatisfied(Clause& c) const {
    for (Clause::VariableConstIterator i = c.getVariableBegin(); i != c.getVariableEnd(); ++i) {
        Variable v = std::abs(*i);
        bool b1 = (*i > 0);
        bool b2 = getParityOfVariable(v);
        if (b1 == b2) {
            return true;
        }
    }
    return false;
}

std::set< Variable > Solution::computeUnsatisfiedVariables(Clause& c, int maxCount) const {
    std::set<Variable> vars;
    int count = 0;
    if (maxCount < c.getNumVariables()) {
        // random-rotate the variable range, so that we pick random maxCount variables and
        // not necessary the first ones. TODO
    }
    for (Clause::VariableConstIterator i = c.getVariableBegin(); i != c.getVariableEnd(); ++i) {
        Variable v = std::abs(*i);
        bool b1 = (*i > 0);
        bool b2 = getParityOfVariable(v);
        if (b1 != b2) {
            vars.insert(v);
            if (count >= maxCount) break;
            else count++;
        }
    }
    return vars;
}

std::ostream& operator<<(std::ostream& os, const Solution& s) {
    std::for_each(s.parity_.begin(), s.parity_.end(), [&](bool b) {
        os << b << ";";
    });
    return os;
}

std::ostream& operator<<(std::ostream& os, const Clause& s) {
    std::for_each(s.variables_.begin(), s.variables_.end(), [&](Variable v) {
        os << v << ",";
    } );
    return os;
}

std::ostream& operator<<(std::ostream& os, const Problem& s) {
    std::for_each(s.allClauses_.begin(), s.allClauses_.end(), [&](Clause* c) {
        os << "<" << *c << "> ";
    } );
    os << " Total " << s.getNumVariables() << " variables.";
    return os;
}
